﻿using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;
using Microsoft.Pex.Framework.Goals;
using Microsoft.Pex.Framework;
using Microsoft.VisualStudio.TestTools.UnitTesting;

namespace MicroBenchmarks.SideEffects
{
    [PexClass]    
    [TestClass]
    public partial class SideEffects
    {
        /// <summary>
        /// An example state where there are no side affects but the internal
        /// state can be achieved by invoking public methods in a certain fashion
        /// (Refer to the factory method to identify the desired sequence)
        /// </summary>
        /// <param name="ifd"></param>
        [PexAssertReachEventually]
        [PexMethod]
        [PexMe.Attribute.FieldAccessObserver]
        [PexMe.Attribute.InsufficientObjectFactoryObserver]
        public void SideEffectsTest([PexAssumeUnderTest]InternalFields ifd)
        {
            //ifd.SetLocalState();
            if (ifd.InternalState)
                PexAssert.ReachEventually();
        }
    }
}
